\batchmode
\makeatletter
\def\input@path{{/Users/sergei.winitzki/Code/talks/ftt-fp/}}
\makeatother
\documentclass[english]{beamer}
\usepackage[T1]{fontenc}
\usepackage[latin9]{inputenc}
\setcounter{secnumdepth}{3}
\setcounter{tocdepth}{3}
\usepackage{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[all]{xy}
\ifx\hypersetup\undefined
  \AtBeginDocument{%
    \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
  }
\else
  \hypersetup{unicode=true,pdfusetitle,
 bookmarks=true,bookmarksnumbered=false,bookmarksopen=false,
 breaklinks=false,pdfborder={0 0 1},backref=false,colorlinks=true}
\fi

\makeatletter
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Textclass specific LaTeX commands.
 % this default might be overridden by plain title style
 \newcommand\makebeamertitle{\frame{\maketitle}}%
 % (ERT) argument for the TOC
 \AtBeginDocument{%
   \let\origtableofcontents=\tableofcontents
   \def\tableofcontents{\@ifnextchar[{\origtableofcontents}{\gobbletableofcontents}}
   \def\gobbletableofcontents#1{\origtableofcontents}
 }
 \newenvironment{lyxcode}
   {\par\begin{list}{}{
     \setlength{\rightmargin}{\leftmargin}
     \setlength{\listparindent}{0pt}% needed for AMS classes
     \raggedright
     \setlength{\itemsep}{0pt}
     \setlength{\parsep}{0pt}
     \normalfont\ttfamily}%
    \def\{{\char`\{}
    \def\}{\char`\}}
    \def\textasciitilde{\char`\~}
    \item[]}
   {\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% User specified LaTeX commands.
\usetheme[secheader]{Boadilla}
\usecolortheme{seahorse}
\title[Chapter 6: Functor-lifted computations I]{Chapter 6: Computations lifted to a functor context I}
\subtitle{Filterable functors, their laws and structure}
\author{Sergei Winitzki}
\date{2018-02-03}
\institute[ABTB]{Academy by the Bay}
\setbeamertemplate{headline}{} % disable headline at top
\setbeamertemplate{navigation symbols}{} % disable navigation bar at bottom
\usepackage[all]{xy}
\makeatletter
% Macros to assist LyX with XYpic with scaling.
\newcommand{\xyScaleX}[1]{%
\makeatletter
\xydef@\xymatrixcolsep@{#1}
\makeatother
} % end of \xyScaleX
\makeatletter
\newcommand{\xyScaleY}[1]{%
\makeatletter
\xydef@\xymatrixrowsep@{#1}
\makeatother
} % end of \xyScaleY

\makeatother

\begin{document}
\frame{\titlepage}
\begin{frame}{Computations within a functor context}

\begin{itemize}
\item Example: 
\[
\sum_{x\in\mathbb{Z};\:0\leq x\leq100;\:\cos x>0}\sqrt{\cos x}\approx38.71
\]
Scala code:

\texttt{\textcolor{blue}{\footnotesize{}(0 to 100).map(math.cos(\_)).filter(\_
> 0).map(math.sqrt).sum}}{\footnotesize \par}
\item Using Scala's \texttt{\textcolor{blue}{\footnotesize{}for}}/\texttt{\textcolor{blue}{\footnotesize{}yield}}
syntax (``functor block'', ``\texttt{\textcolor{blue}{\footnotesize{}for}}
comprehension'')

\texttt{\textcolor{blue}{\footnotesize{}}}%
\begin{minipage}[t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}(for~\{~x~$\leftarrow$~0~to~100}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~y~=~math.cos(x)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~if~y~>~0}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~\}~yield~math.sqrt(y)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}).sum}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}\texttt{\textcolor{blue}{\footnotesize{}}}%
\begin{minipage}[t]{0.49\columnwidth}%
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}(0~to~100).map~\{~x~$\Rightarrow$}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~math.cos(x)~\}.filter~\{~y~$\Rightarrow$}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~y~>~0~\}.map~\{~y~$\Rightarrow$}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~~math.sqrt(y)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~\}.sum}{\footnotesize \par}
\end{lyxcode}
%
\end{minipage}{\footnotesize \par}
\begin{itemize}
\item ``Functor block'' is a syntax for manipulating data within a container
\begin{itemize}
\item Container must be a functor (has \texttt{\textcolor{blue}{\footnotesize{}map}}
such that the laws hold)
\item Data changes but remains within the same container 
\end{itemize}
\end{itemize}
\item A \textbf{filterable functor} is a functor that has a \texttt{\textcolor{blue}{\footnotesize{}withFilter}}
method
\item Can use ``\texttt{\textcolor{blue}{\footnotesize{}if}}'' when \texttt{\textcolor{blue}{\footnotesize{}withFilter(p:\ A$\Rightarrow$Boolean):\ F{[}A{]}
$\Rightarrow$ F{[}A{]}}} is defined
\begin{itemize}
\item What are the required laws for \texttt{\textcolor{blue}{\footnotesize{}withFilter}}?
\item What data types are filterable functors?
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Filterable functors: Intuitions I}

Intuition: the \texttt{\textcolor{blue}{\footnotesize{}filter}} call
\emph{may decrease} the number of data items held
\begin{itemize}
\item a filterable container can hold \emph{more or fewer} data items of
type $T$
\end{itemize}
Examples:
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}Option{[}T{]}}} $\equiv1+T$
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}Some(123).filter(\_ > 0)}}
returns \texttt{\textcolor{blue}{\footnotesize{}Some(123)}} 
\item \texttt{\textcolor{blue}{\footnotesize{}Some(123).filter(\_ == 1)}}
returns \texttt{\textcolor{blue}{\footnotesize{}None}} 
\item \texttt{\textcolor{blue}{\footnotesize{}Some(123).withFilter(\_ ==
1).map(identity)}} returns \texttt{\textcolor{blue}{\footnotesize{}None}} 
\end{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}List{[}T{]}}} $\equiv1+T+T\times T+T\times T\times T+...$
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}List(10, 20, 30).filter(\_
> 10)}} returns \texttt{\textcolor{blue}{\footnotesize{}List(20, 30)}} 
\item \texttt{\textcolor{blue}{\footnotesize{}List(10, 20, 30).filter(\_
== 1)}} returns \texttt{\textcolor{blue}{\footnotesize{}List()}} 
\end{itemize}
\end{itemize}
What we learn from these examples:
\begin{itemize}
\item The data type must contain a \emph{disjunction} having different counts
of $T$
\item When the predicate \texttt{\textcolor{blue}{\footnotesize{}p}} returns
\texttt{\textcolor{blue}{\footnotesize{}false}} on some $T$ values,
the remaining data goes to a part of the disjunction that has fewer
$T$ values
\item Values \texttt{\textcolor{blue}{\footnotesize{}x}} are \emph{algebraically}
replaced by $1$ (a \texttt{\textcolor{blue}{\footnotesize{}Unit}})
when \texttt{\textcolor{blue}{\footnotesize{}p(x) = false}} 
\item The container can become ``empty'' as a result of filtering
\end{itemize}
\end{frame}

\begin{frame}{Examples of filterable functors I}

\begin{itemize}
\item Consider these business requirements:
\begin{itemize}
\item An order can be placed on Tuesday and/or on Friday
\item An order is approved under certain conditions (amount < \$1000, etc.)
\end{itemize}
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}final~case~class~Orders{[}A{]}(tue:~Option{[}A{]},~fri:~Option{[}A{]})~\{}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~def~withFilter(p:~A~$\Rightarrow$~Boolean):~Orders{[}A{]}~=~}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~~~Orders(tue.filter(p),~fri.filter(p))}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}Orders(Some(500),~Some(2000)).withFilter(\_~<~1000)}{\footnotesize \par}

\textrm{\textcolor{darkgray}{\footnotesize{}//~returns~}}\textcolor{darkgray}{\footnotesize{}Orders(Some(500),~None)}\textrm{\textcolor{darkgray}{\footnotesize{}~\textendash{}~see~example~code}}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item This functor type is written as $F^{A}=(1+A)\times(1+A)$
\begin{itemize}
\item When a value does not pass the filter, the $A$ is replaced by $1$
\end{itemize}
\item Filtering is applied independently to both parts of the product type
\item What if additional business requirements were given:
\begin{itemize}
\item (a) both orders must be approved, or else no orders can be placed\\
or
\item (b) both orders can be placed if at least one of them is approved
\end{itemize}
\item Does this still make sense as ``filtering''?
\begin{itemize}
\item Need mathematical laws to decide this
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Filterable functors: Intuitions II}

\begin{itemize}
\item Intuition: computations in the functor block should ``make sense''
\begin{itemize}
\item we should be able to reason correctly by looking at the program text
\end{itemize}
\item A schematic example of a functor block program using \texttt{\textcolor{blue}{\footnotesize{}map}}
and \texttt{\textcolor{blue}{\footnotesize{}filter}}:
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}for~\{~}\textrm{\textcolor{darkgray}{\footnotesize{}//~computations~lifted~into~the~}}\textcolor{darkgray}{\footnotesize{}List}\textrm{\textcolor{darkgray}{\footnotesize{}~functor}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~x~$\leftarrow$~List(...)~}\textrm{\textcolor{darkgray}{\footnotesize{}//~the~first~line~has~``$\leftarrow$'',~other~lines~do~not}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~y~=~f(x)~}\textrm{\textcolor{darkgray}{\footnotesize{}//~will~become~a~``}}\textcolor{darkgray}{\footnotesize{}map(f)}\textrm{\textcolor{darkgray}{\footnotesize{}''~after~compilation}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~if~p1(y)~}\textrm{\textcolor{darkgray}{\footnotesize{}//~will~become~a~``}}\textcolor{darkgray}{\footnotesize{}withFilter(p1)}\textrm{\textcolor{darkgray}{\footnotesize{}''}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~if~p2(y)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~z~=~g(x,~y)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~if~q(x,~y,~z)}\textrm{\textcolor{darkgray}{\footnotesize{}~//~\textendash{}~more~conditions,~etc.;~see~example~code}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}\}~yield~}\textrm{\textcolor{darkgray}{\footnotesize{}//~~for~all~}}\textcolor{darkgray}{\footnotesize{}x}\textrm{\textcolor{darkgray}{\footnotesize{}~in~list,~such~that~conditions~hold,~compute~this:}}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~k(x,~y,~z)~}\textrm{\textcolor{darkgray}{\footnotesize{}//~~all~the~new~values~will~stay~within~the~container}}{\footnotesize \par}
\end{lyxcode}
\item What we intuitively expect to be true about such programs:
\begin{enumerate}
\item \texttt{\textcolor{blue}{\footnotesize{}y = f(x); if p(y);}} is equivalent
to \texttt{\textcolor{blue}{\footnotesize{}if p(f(x)); y = f(x);}} 
\item \texttt{\textcolor{blue}{\footnotesize{}if p1(y); if p2(y);}} is equivalent
to \texttt{\textcolor{blue}{\footnotesize{}if p1(y) \&\& p2(y)}} 
\item When a filter predicate \texttt{\textcolor{blue}{\footnotesize{}p(x)}}
returns \texttt{\textcolor{blue}{\footnotesize{}true}} for \emph{all}
\texttt{\textcolor{blue}{\footnotesize{}x}}, we can delete the line
``\texttt{\textcolor{blue}{\footnotesize{}if p(x)}}'' from the program
with no change to the results
\item When a filter predicate \texttt{\textcolor{blue}{\footnotesize{}p(x)}}
returns \texttt{\textcolor{blue}{\footnotesize{}false}} for some \texttt{\textcolor{blue}{\footnotesize{}x}}
then\emph{ that} \texttt{\textcolor{blue}{\footnotesize{}x}} will
be excluded from computations performed after ``\texttt{\textcolor{blue}{\footnotesize{}if
p(x)}}''
\end{enumerate}
\end{itemize}
\end{frame}

\begin{frame}{Examples of filterable functors II: Checking the laws}

\begin{itemize}
\item Properties 1 \textendash{} 4 are expressed as laws for \texttt{\textcolor{blue}{\footnotesize{}filter}}$^{(p\Rightarrow\text{Boolean})\Rightarrow F^{A}\Rightarrow F^{A}}$:
\begin{enumerate}
\item {\footnotesize{}$\text{fmap}\,f^{A\Rightarrow B}\circ\text{filter}\,p^{B\Rightarrow\text{Boolean}}=\text{filter}\left(f\circ p\right)\circ\text{fmap}\,f^{A\Rightarrow B}$}{\footnotesize \par}
\item {\footnotesize{}$\text{filter}\,p_{1}^{A\Rightarrow\text{Boolean}}\circ\text{filter}\,p_{2}^{A\Rightarrow\text{Boolean}}=\text{filter}\left(x\Rightarrow p_{1}(x)\wedge p_{2}(x)\right)$}{\footnotesize \par}
\item {\footnotesize{}$\text{filter}\left(x^{A}\Rightarrow\text{true}\right)=\text{id}^{F^{A}\Rightarrow F^{A}}$ }{\footnotesize \par}
\item {\footnotesize{}$\text{filter}\,p\circ\text{fmap}\,f^{A\Rightarrow B}=\text{filter}\,p\circ\text{fmap}\left(f_{|p}\right)$
}where {\footnotesize{}$f_{|p}$} is the \emph{partial function} defined
as \texttt{\textcolor{blue}{\footnotesize{}\{ case x if p(x) $\Rightarrow$
f(x) \}}} \textendash{} only works if $p(x)$ holds
\end{enumerate}
\item Can define a type class \texttt{\textcolor{blue}{\footnotesize{}Filterable}},
method \texttt{\textcolor{blue}{\footnotesize{}withFilter}} 
\item Check the laws for the \texttt{\textcolor{blue}{\footnotesize{}Orders}}
functor (see example code)
\begin{itemize}
\item Laws hold for the \texttt{\textcolor{blue}{\footnotesize{}Orders}}
functor with / without business rule (a)
\item Another filterable functor: $F^{A}\equiv1+A\times A$ (``collapsible
product'')
\end{itemize}
\item Examples of functors that are \emph{not} filterable:
\begin{itemize}
\item ``Orders'' with additional business rule (b) \textendash{} breaks
law 2 for some $p_{1,2}$
\item $F^{A}$ defining \texttt{\textcolor{blue}{\footnotesize{}filter}}
in a special way e.g.~for $A=\text{Int}$ \textendash{} breaks law
1
\item $F^{A}\equiv1+A$ defining $\text{filter}\left(p\right)\left(x\right)\equiv1+0$
breaks law 3
\item $F^{A}\equiv A$ \textendash{} must define $\text{filter}\left(p^{A\Rightarrow\text{Boolean}}\right)\left(x^{A}\right)=x$,
breaking law 4
\item $F^{A}\equiv A\times\left(1+A\right)$ \textendash{} unable to remove
the first $A$, breaking law 4
\end{itemize}
\end{itemize}
The equational laws 1\textendash 4 specify \emph{rigorously} what
it means to ``filter data''!
\end{frame}

\begin{frame}{Worked examples I: Programming with filterables}
\begin{enumerate}
\item John can have up to 3 coupons, and Jill up to 2. \emph{All} of John's
coupons must be valid on purchase day, while each of Jill's coupons
is checked independently. Implement the filterable functor describing
this setup.
\item A server received a sequence of requests. Each request must be authenticated.
Once a non-authenticated request is found, no further requests are
accepted. Is this setup described by a filterable functor?\\
\ \\
For each of these functors, determine whether they are filterable,
and if so, implement \texttt{\textcolor{blue}{\footnotesize{}withFilter}}
via a type class:
\item \texttt{\textcolor{blue}{\footnotesize{}final case class P{[}T{]}(first:\ Option{[}T{]},
second:\ Option{[}(T, T){]})}}{\footnotesize \par}
\item $F^{A}\equiv\text{Int}+\text{Int}\times A+\text{Int}\times A\times A+\text{Int}\times A\times A\times A$
\item $F^{A}=\text{NonEmptyList}^{A}$ defined recursively as $F^{A}\equiv A+A\times F^{A}$ 
\item $F^{Z,A}\equiv Z+\text{Int}\times Z\times A\times A$ (with respect
to the type parameter $A$)
\item $F^{Z,A}\equiv1+Z+\text{Int}\times A\times\text{List}^{A}$ (w.r.t.\ the
type parameter $A$)
\item {*} Show that $C^{Z,A}=A\Rightarrow1+Z$ is a filterable \emph{contrafunctor}
w.r.t.\ $A$ (implement \texttt{\textcolor{blue}{\footnotesize{}withFilter}}
with the same type signature; no law checking)
\end{enumerate}
\end{frame}

\begin{frame}{Exercises I}
\begin{enumerate}
\item Confucius gave wisdom on each of the 7 days of a week. Sometimes the
wise proverbs were hard to remember. If Confucius forgets what he
said on a given day, he also forgets what he said on all the previous
days of the week. Is this setup described by a filterable functor?
\item Define \texttt{\textcolor{blue}{\footnotesize{}evenFilter(p)}} on
an \texttt{\textcolor{blue}{\footnotesize{}IndexedSeq{[}T{]}}} such
that a value \texttt{\textcolor{blue}{\footnotesize{}x:\ T}} is retained
if \texttt{\textcolor{blue}{\footnotesize{}p(x)=true}} \emph{and}
only if the sequence has an \emph{even} number of elements \texttt{\textcolor{blue}{\footnotesize{}y}}
for which \texttt{\textcolor{blue}{\footnotesize{}p(y)=false}}. Does
this define a filterable functor?\\
\ \\
Implement \texttt{\textcolor{blue}{\footnotesize{}filter}} for these
functors if possible (law checking optional):
\item $F^{A}\equiv\text{Int}+\text{String}\times A\times A\times A$
\item \texttt{\textcolor{blue}{\footnotesize{}final case class Q{[}A, Z{]}(id:\ Long,
user1:\ Option{[}(A, Z){]}, user2:\ Option{[}(A, Z){]}) }}\textendash{}
with respect to the type parameter $A$
\item $F^{A}=\text{MyTree}^{A}$ defined recursively as $F^{A}\equiv1+A\times F^{A}\times F^{A}$
\item \texttt{\textcolor{blue}{\footnotesize{}final case class R{[}A{]}(x:\ Int,\ y: Int,
z:\ A, data:\ List{[}A{]})}}, where the standard functor $\text{List}$
already has \texttt{\textcolor{blue}{\footnotesize{}withFilter}} defined
\item {*} Show that $C^{A}\equiv A+A\times A\Rightarrow1+Z$ is a filterable
contrafunctor
\end{enumerate}
\end{frame}

\begin{frame}{Filterable functors: The laws in depth I}

Is there a shorter formulation of the laws that is easier to remember?
\begin{itemize}
\item Intuition: When \texttt{\textcolor{blue}{\footnotesize{}p(x) = false}},
replace \texttt{\textcolor{blue}{\footnotesize{}x:\ A}} by \texttt{\textcolor{blue}{\footnotesize{}1:\ Unit}}
in \texttt{\textcolor{blue}{\footnotesize{}F{[}A{]}}} 
\begin{itemize}
\item (1) How to replace \texttt{\textcolor{blue}{\footnotesize{}x}} by
\texttt{\textcolor{blue}{\footnotesize{}1}} in \texttt{\textcolor{blue}{\footnotesize{}F{[}A{]}}}
without breaking the types?
\item (2) How to transform the resulting type back to \texttt{\textcolor{blue}{\footnotesize{}F{[}A{]}}}?
\end{itemize}
\item We could do (1) if instead of $F^{A}$ we had $F^{1+A}$ i.e.~\texttt{\textcolor{blue}{\footnotesize{}F{[}Option{[}A{]}{]}}} 
\begin{itemize}
\item Now use \texttt{\textcolor{blue}{\footnotesize{}filter}} to replace
$A$ by $1$ in each item of type $1+A$
\item Get $F^{1+A}$ from $F^{A}$ using $\text{inflate}:F^{A}\Rightarrow F^{1+A}=\text{fmap}\,(\text{Some}^{A\Rightarrow1+A})$ 
\item Filter $F^{1+A}\Rightarrow F^{1+A}$ using $\text{fmap}\left(x^{1+A}\Rightarrow\text{filter}_{\text{Opt}}(p^{A\Rightarrow\text{Boolean}})(x)\right)$
\end{itemize}
\[
\text{filter}\,p:\xymatrix{\xyScaleX{5pc}F^{A}\ar[r]\sb(0.45){\text{inflate}} & F^{1+A}\ar[r]_{\text{fmap}\left(\text{filter}_{\text{Opt}}p\right)} & F^{1+A}\ar[r]\sb(0.55){\text{deflate}} & F^{A}}
\]

\item Doing (2) means \emph{defining} a function \texttt{\textcolor{blue}{\footnotesize{}deflate:\ F{[}Option{[}A{]}{]}
$\Rightarrow$ F{[}A{]}}} 
\begin{itemize}
\item standard library already has \texttt{\textcolor{blue}{\footnotesize{}flatten{[}T{]}:\ Seq{[}Option{[}T{]}{]}
$\Rightarrow$ Seq{[}T{]}}} 
\end{itemize}
\item Simplify{\footnotesize{} $\text{fmap}(\text{Some}^{A\Rightarrow1+A})\circ\text{fmap}\left(\text{filter}_{\text{Opt}}p\right)=\text{fmap}\left(\text{bop}\left(p\right)\right)$}
where we defined {\footnotesize{}$\text{{\color{blue}bop}}\left(p\right):\left(A\Rightarrow1+A\right)\equiv$}
\texttt{\textcolor{blue}{\footnotesize{}x $\Rightarrow$ Some(x).filter(p)}} 
\item In this way, express \texttt{\textcolor{blue}{\footnotesize{}filter}}
through \texttt{\textcolor{blue}{\footnotesize{}deflate}} (see example
code)
\begin{itemize}
\item $\text{filter}\,p=\text{fmap}\left(\text{bop}\,p\right)\circ\text{deflate}$.
\textendash{} Notation: $\text{bop}\,p$ is $\text{bop}\left(p\right)$,
like $\cos x$
\end{itemize}
\[
\text{filter}\:p:\xymatrix{\xyScaleX{5pc}F^{A}\ar[r]\sb(0.45){\text{fmap}\left(\text{bop}\,p\right)} & F^{1+A}\ar[r]\sb(0.55){\text{deflate}} & F^{A}}
\]

\end{itemize}
\end{frame}

\begin{frame}{Filterable functors: Using \texttt{\textcolor{blue}{\footnotesize{}deflate}}}

\begin{itemize}
\item So far we have expressed \texttt{\textcolor{blue}{\footnotesize{}filter}}
through \texttt{\textcolor{blue}{\footnotesize{}deflate}} 
\item We can also express \texttt{\textcolor{blue}{\footnotesize{}deflate}}
through \texttt{\textcolor{blue}{\footnotesize{}filter}} (assuming
law 4 holds):

\[
\text{deflate}:\xymatrix{\xyScaleX{5pc}F^{1+A}\ar[r]\sb(0.5){\text{filter}\left(\text{.nonEmpty}\right)} & F^{1+A}\ar[r]\sb(0.5){\text{fmap}\left(\text{.get}\right)} & F^{A}}
\]

\begin{lyxcode}
\textcolor{blue}{\footnotesize{}def~deflate{[}F{[}\_{]},A{]}(foa:~F{[}Option{[}A{]}{]}):~F{[}A{]}~=}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}~~foa.filter(\_.nonEmpty).map(\_.get)~}\textrm{\textcolor{gray}{\footnotesize{}//~}}\textcolor{gray}{\footnotesize{}\_.get}\textrm{\textcolor{gray}{\footnotesize{}~is~$0+x^{A}\Rightarrow x^{A}$}}{\footnotesize \par}

\textrm{\textcolor{gray}{\footnotesize{}//~for~}}\textcolor{gray}{\footnotesize{}F~=~Seq}\textrm{\textcolor{gray}{\footnotesize{},~this~would~be~}}\textcolor{gray}{\footnotesize{}foa.collect~\{~case~Some(x)~$\Rightarrow$~x~\}}{\footnotesize \par}

\textrm{\textcolor{gray}{\footnotesize{}//~for~arbitrary~functor~}}\textcolor{gray}{\footnotesize{}F}\textrm{\textcolor{gray}{\footnotesize{}~we~need~to~use~the~partial~function,~}}\textcolor{gray}{\footnotesize{}\_.get}{\footnotesize \par}
\end{lyxcode}
\item This means \texttt{\textcolor{blue}{\footnotesize{}deflate}} and \texttt{\textcolor{blue}{\footnotesize{}filter}}
are \textbf{computationally equivalent}
\begin{itemize}
\item We could specify filterable functors by implementing \texttt{\textcolor{blue}{\footnotesize{}deflate}} 
\begin{itemize}
\item The implementation of \texttt{\textcolor{blue}{\footnotesize{}filter}}
would then be derived by library
\end{itemize}
\end{itemize}
\item Use \texttt{\textcolor{blue}{\footnotesize{}deflate}} to verify that
some functors are certainly not filterable:
\begin{itemize}
\item $F^{A}=A+A\times A$. Write $F^{1+A}=1+A+(1+A)\times(1+A)$ 
\begin{itemize}
\item cannot map $F^{1+A}\Rightarrow F^{A}$ because we do not have $1\rightarrow A$
\end{itemize}
\item $F^{A}=\text{Int}\Rightarrow A$. Write $F^{1+A}=\text{Int}\Rightarrow1+A$ 
\begin{itemize}
\item type signature of \texttt{\textcolor{blue}{\footnotesize{}deflate}}
would be $\left(\text{Int}\Rightarrow1+A\right)\Rightarrow\text{Int}\Rightarrow A$
\item cannot map $F^{1+A}\Rightarrow F^{A}$ because we do not have $1+A\rightarrow A$
\end{itemize}
\end{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}deflate}} is easier to implement
and to reason about
\end{itemize}
\end{frame}

\begin{frame}{{*} Filterable functors: The laws in depth II}

\begin{itemize}
\item We were able to define \texttt{\textcolor{blue}{\footnotesize{}deflate}}
only by assuming that law 4 holds
\item Now, law 4 is satisfied \emph{automatically} if \texttt{\textcolor{blue}{\footnotesize{}filter}}
is defined via \texttt{\textcolor{blue}{\footnotesize{}deflate}}!
\begin{itemize}
\item Denote {\footnotesize{}$\psi_{p}^{F^{A}\Rightarrow F^{1+A}}\equiv\text{fmap}\left(\text{bop}\:p\right)$
for brevity, then $\text{filter}\,p=\psi_{p}\circ\text{deflate}$}{\footnotesize \par}
\item Law 4 then becomes: {\footnotesize{}$\psi_{p}\circ\text{deflate}\circ\text{fmap}\:f^{A\Rightarrow B}=\psi_{p}\circ\text{deflate}\circ\text{fmap}\:f_{|p}$
\[
\xymatrix{\xyScaleY{0.1pc}\xyScaleX{3pc} & F^{1+A}\ar[r]\sp(0.5){\text{deflate}} & F^{A}\ar[rd]\sp(0.5){\text{ fmap}\:f^{A\Rightarrow B}}\\
F^{A}\ar[ru]\sp(0.5){\psi_{p}}\ar[rd]\sb(0.5){\psi_{p}} &  &  & F^{B}\\
 & F^{1+A}\ar[r]\sb(0.5){\text{deflate}} & F^{A}\ar[ru]\sb(0.5){\text{fmap}\:f_{|p}^{A\Rightarrow B}}
}
\]
}{\footnotesize \par}
\end{itemize}
\item We would like to interchange \texttt{\textcolor{blue}{\footnotesize{}deflate}}
and \texttt{\textcolor{blue}{\footnotesize{}fmap}} in both sides
\begin{itemize}
\item We need a \emph{naturality} law; let's express law 1 through \texttt{\textcolor{blue}{\footnotesize{}deflate}}:
\end{itemize}
\end{itemize}
{\footnotesize{}
\[
\text{fmap}\:f^{A\Rightarrow B}\circ\psi_{p}\circ\text{deflate}^{F,B}=\psi_{f\circ p}\circ\text{deflate}^{F,A}\circ\text{fmap}\:f^{A\Rightarrow B}
\]
\[
\xymatrix{\xyScaleY{0.1pc}\xyScaleX{3pc} & F^{B}\ar[r]\sp(0.5){\psi_{p}} & F^{1+B}\ar[rd]\sp(0.5){\text{ deflate}^{F,B}}\\
F^{A}\ar[ru]\sp(0.5){\text{fmap}\:f^{A\Rightarrow B}}\ar[rd]\sb(0.5){\psi_{f\circ p}} &  &  & F^{B}\\
 & F^{1+A}\ar[r]\sb(0.5){\text{deflate}^{F,A}} & F^{A}\ar[ru]\sb(0.5){\text{fmap}\:f^{A\Rightarrow B}}
}
\]
Can we simplify $\text{fmap}\:f\circ\psi_{p}=\text{fmap}\:f\circ\text{fmap}\left(\text{bop}\,p\right)=\text{fmap}\left(f\circ\text{bop}\,p\right)$?}{\footnotesize \par}
\end{frame}

\begin{frame}{{*} Filterable functors: The laws in depth III}

\begin{itemize}
\item {\footnotesize{}Have property: $f^{A\Rightarrow B}\circ\text{bop}\left(p^{B\Rightarrow\text{Boolean}}\right)=\text{bop}\left(f\circ p\right)\circ\text{fmap}^{\text{Opt}}\,f$
(see code)
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & B\ar[rd]\sp(0.5){\text{bop}\,p}\\
A\ar[ru]\sp(0.5){f^{A\Rightarrow B}}\ar[rd]\sb(0.4){\text{bop}\left(f\circ p\right)\,} &  & 1+B\\
 & 1+A\ar[ru]\sb(0.6){\text{fmap}^{\text{Opt}}f}
}
\]
We can now rewrite Law 1 as
\[
\text{fmap}\,(\text{bop}\left(f\circ p\right))\circ\text{fmap}\,(\text{fmap}^{\text{Opt}}f)\circ\text{deflate}=\text{fmap}\left(\text{bop}\left(f\circ p\right)\right)\circ\text{deflate}\circ\text{fmap}\,f
\]
Remove common prefix $\text{fmap}\left(\text{bop}\left(f\circ p\right)\right)\circ...$
from both sides:
\[
\text{fmap}\,(\text{fmap}^{\text{Opt}}f^{A\Rightarrow B})\circ\text{deflate}^{F,B}=\text{deflate}^{F,A}\circ\text{fmap}\,f^{A\Rightarrow B}\ \ -\text{ \textbf{law 1 for deflate}}
\]
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & F^{1+B}\ar[rd]\sp(0.5){\ \text{deflate}^{F,B}}\\
F^{1+A}\ar[ru]\sp(0.5){\text{fmap}\,(\text{fmap}\,f)\ }\ar[rd]\sb(0.5){\text{deflate}^{F,A}\,} &  & F^{B}\\
 & F^{A}\ar[ru]\sb(0.5){\text{fmap\,}f^{A\Rightarrow B}}
}
\]
}{\footnotesize \par}
\item \texttt{\textcolor{blue}{\footnotesize{}deflate}}{\footnotesize{}$:F^{1+A}\Rightarrow F^{A}$}
 is a \textbf{natural transformation} (has naturality law)
\begin{itemize}
\item Example:{\footnotesize{} $F^{A}=1+A\times A$}{\footnotesize \par}
\item {\footnotesize{}$F^{1+A}=1+(1+A)\times(1+A)=1+1\times1+A\times1+1\times A+A\times A$}{\footnotesize \par}
\end{itemize}
\item {\footnotesize{}natural transformations map containers $G^{A}\Rightarrow H^{A}$
by rearranging data in them}{\footnotesize \par}
\end{itemize}
\end{frame}

\begin{frame}{{*} Filterable functors: The laws in depth IV}

\begin{itemize}
\item The naturality law for \texttt{\textcolor{blue}{\footnotesize{}deflate}}:{\footnotesize{}
\[
\text{fmap}\,(\text{fmap}^{\text{Opt}}f^{A\Rightarrow B})\circ\text{deflate}^{F,B}=\text{deflate}^{F,A}\circ\text{fmap}\,f^{A\Rightarrow B}
\]
}Law 4 expressed via \texttt{\textcolor{blue}{\footnotesize{}deflate}}:{\footnotesize{}
\[
\xymatrix{\xyScaleY{0.1pc}\xyScaleX{3pc} & F^{1+A}\ar[r]\sp(0.5){\text{deflate}} & F^{A}\ar[rd]\sp(0.5){\text{ fmap}\:f^{A\Rightarrow B}}\\
F^{A}\ar[ru]\sp(0.5){\psi_{p}}\ar[rd]\sb(0.5){\psi_{p}} &  &  & F^{B}\\
 & F^{1+A}\ar[r]\sb(0.5){\text{deflate}} & F^{A}\ar[ru]\sb(0.5){\text{fmap}\:f_{|p}^{A\Rightarrow B}}
}
\]
\[
\psi_{p}\circ\text{deflate}^{F,A}\circ\text{fmap}\:f^{A\Rightarrow B}=\psi_{p}\circ\text{deflate}^{F,A}\circ\text{fmap}\:f_{|p}
\]
}{\footnotesize \par}
\item Use naturality to interchange \texttt{\textcolor{blue}{\footnotesize{}deflate}}
and \texttt{\textcolor{blue}{\footnotesize{}fmap}} in both sides of
law 4:{\footnotesize{}
\begin{align*}
\psi_{p}\circ\text{fmap}\,(\text{fmap}^{\text{Opt}}f)\circ\text{deflate}^{F,B} & =\psi_{p}\circ\text{fmap}\,(\text{fmap}^{\text{Opt}}f_{|p})\circ\text{deflate}^{F,B}\\
\text{[omit }\text{deflate}^{F,B}\text{ from} & \ \text{both sides; expand }\psi_{p}\text{]}\\
\text{bop}\,p\circ\text{fmap}^{\text{Opt}}f & =\text{bop}\,p\circ\text{fmap}^{\text{Opt}}f_{|p}\ \ -\text{ check this by hand:}
\end{align*}
}{\footnotesize \par}
\end{itemize}
\begin{lyxcode}
\textcolor{blue}{\footnotesize{}x~$\Rightarrow$~Some(x).filter(p).map(f)}{\footnotesize \par}

\textcolor{blue}{\footnotesize{}x~$\Rightarrow$~Some(x).filter(p).map~\{~case~x~if~p(x)~$\Rightarrow$~\{~case~x~if~p(x)~$\Rightarrow$~f(x)~\}}{\footnotesize \par}
\end{lyxcode}
\begin{itemize}
\item These functions are equivalent because law 4 holds for \texttt{\textcolor{blue}{\footnotesize{}Option}}{\footnotesize \par}
\end{itemize}
\end{frame}

\begin{frame}{Filterable functors: The laws in depth V}

Maybe $\psi_{p}\circ\text{deflate}$ is easier to handle than \texttt{\textcolor{blue}{\footnotesize{}deflate}}?
Let us define {\footnotesize{}
\[
\text{{\color{blue}fmapOpt}}^{F,A,B}(f^{A\Rightarrow1+B}):F^{A}\Rightarrow F^{B}=\text{fmap}\:f\circ\text{deflate}^{F,B}
\]
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & F^{1+B}\ar[rd]\sp(0.5){\ \text{deflate}^{F,B}}\\
F^{A}\ar[ru]\sp(0.5){\text{fmap}\,f^{A\Rightarrow1+B}\ }\ar[rr]\sb(0.5){\text{fmapOpt}\:f^{A\Rightarrow1+B}\,} &  & F^{B}
}
\]
}{\footnotesize \par}
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}} and \texttt{\textcolor{blue}{\footnotesize{}deflate}}
are \emph{equivalent}: {\footnotesize{}$\text{deflate}^{F,A}=\text{fmapOpt}^{F,1+A,A}(\text{id}^{1+A\Rightarrow1+A})$ }{\footnotesize \par}
\item Express laws 1 \textendash{} 3 in terms of \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}}:
do they get simpler?
\begin{itemize}
\item Express \texttt{\textcolor{blue}{\footnotesize{}filter}} through \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}}:
{\footnotesize{}$\text{filter}\,p=\text{fmapOpt}^{F,A,A}\left(\text{bop}\,p\right)$}{\footnotesize \par}
\item Consider the expression needed for law 2: $x\Rightarrow p_{1}(x)\wedge p_{2}(x)$
\item {\footnotesize{}$\text{bop}\left(x\Rightarrow p_{1}(x)\wedge p_{2}(x)\right)=x^{A}\Rightarrow\left(\text{bop}\,p_{1}\right)(x)\text{.flatMap}\left(\text{bop}\,p_{2}\right)$
}\textendash{} see code
\begin{itemize}
\item Denote this computation by $\diamond_{\text{Opt}}$ and write{\footnotesize{}
\[
q_{1}^{A\Rightarrow1+B}\diamond_{\text{Opt}}q_{2}^{B\Rightarrow1+C}\equiv x^{A}\Rightarrow q_{1}(x).\text{flatMap}\left(q_{2}\right)
\]
}{\footnotesize \par}
\end{itemize}
\item Similar to composition of functions, except the types are $A\Rightarrow1+B$
\begin{itemize}
\item This is a particular case of \textbf{Kleisli composition}; the general
case: {\footnotesize{}$\diamond_{M}:(A\Rightarrow M^{B})\Rightarrow(B\Rightarrow M^{C})\Rightarrow(A\Rightarrow M^{C})$};
we set $M^{A}\equiv1+A$
\item The \textbf{Kleisli identity} function: $\text{id}_{\diamond_{\text{Opt}}}^{A\Rightarrow1+A}\equiv x^{A}\Rightarrow\text{Some}\left(x\right)$
\item Kleisli composition $\diamond_{\text{Opt}}$ is associative and respects
the Kleisli identity!
\item \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}} lifts a Kleisli$_{\text{Opt}}$
function $f^{A\Rightarrow1+B}$ into the functor $F$
\end{itemize}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Filterable functors: The laws in depth VI}


\framesubtitle{Simplifying down to two laws}
\begin{itemize}
\item Only \emph{two} laws are necessary for \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}}!
\end{itemize}
\begin{enumerate}
\item \textbf{Identity law} (covers old law 3): {\footnotesize{}
\[
\text{fmapOpt}\,(\text{id}_{\diamond_{\text{Opt}}}^{A\Rightarrow1+A})=\text{id}^{F^{A}\Rightarrow F^{A}}
\]
}{\footnotesize \par}
\item \textbf{Composition law} (covers old laws 1 and 2): {\footnotesize{}
\[
\text{fmapOpt}\,(f^{A\Rightarrow1+B})\circ\text{fmapOpt}\,(g^{B\Rightarrow1+C})=\text{fmapOpt}\left(f\diamond_{\text{\textbf{Opt}}}g\right)
\]
\[
\xymatrix{\xyScaleY{2pc}\xyScaleX{3pc} & F^{B}\ar[rd]\sp(0.55){\ \text{fmapOpt}\,(g^{B\Rightarrow1+C})}\\
F^{A}\ar[ru]\sp(0.45){\text{fmapOpt}\,(f^{A\Rightarrow1+B})\ }\ar[rr]\sb(0.5){\text{fmapOpt}\left(f\diamond_{\text{Opt}}g\right)} &  & F^{C}
}
\]
}{\footnotesize \par}
\end{enumerate}
\begin{itemize}
\item The two laws for \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}}
are very similar to the two functor laws
\begin{itemize}
\item Both of them use more complicated types than the old laws
\item Conceptually, the new laws are simpler (lift $f^{A\Rightarrow1+B}$
into $F^{A}\Rightarrow F^{B}$)
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{{*} Filterable functors: The laws in depth VII}


\framesubtitle{Showing that old laws 1 \textendash{} 3 follow from the identity
and composition laws for \texttt{\footnotesize{}fmapOpt}}
\begin{itemize}
\item Old law 3 is \emph{equivalent} to the identity law for \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}}:{\footnotesize{}
\[
\text{filter}\,(x^{A}\Rightarrow\text{true})=\text{fmap}\,(x^{A}\Rightarrow0+x)\circ\text{deflate}=\text{fmapOpt}\,(\text{id}_{\diamond_{\text{Opt}}})=\text{id}^{F^{A}\Rightarrow F^{A}}
\]
}{\footnotesize \par}
\item Derive old law 2: need to work with{\footnotesize{} $q_{1,2}\equiv\text{bop}\left(p_{1,2}\right):A\Rightarrow1+A$ }{\footnotesize \par}
\begin{itemize}
\item The Boolean conjunction {\footnotesize{}$x\Rightarrow p_{1}(x)\wedge p_{2}(x)$
}corresponds to {\footnotesize{}$q_{1}\diamond_{\text{\textbf{Opt}}}q_{2}$}{\footnotesize \par}
\item Apply the composition law to Kleisli functions of types {\footnotesize{}$A\Rightarrow1+A$
}:{\footnotesize{}
\begin{align*}
\text{filter}\,p_{1}\circ\text{filter}\,p_{2} & =\text{fmapOpt}\,q_{1}\circ\text{fmapOpt}\,q_{2}\\
=\text{fmapOpt}\left(q_{1}\diamond_{\text{\textbf{Opt}}}q_{2}\right) & =\text{fmapOpt}\left(\text{bop}\left(x\Rightarrow p_{1}(x)\wedge p_{2}(x)\right)\right)
\end{align*}
}{\footnotesize \par}
\end{itemize}
\item Derive old law 1:
\begin{itemize}
\item express \texttt{\textcolor{blue}{\footnotesize{}filter}} through \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}};
old law 1 becomes{\footnotesize{}
\[
\text{fmap}\:f\circ\text{fmapOpt}\left(\text{bop}\,p\right)=\text{fmapOpt}\left(\text{bop}\left(f\circ p\right)\right)\circ\text{fmap}\:f\ \text{ \textendash\ eq. (*)}
\]
}{\footnotesize \par}
\item lift $f^{A\Rightarrow B}$ to Kleisli$_{\text{Opt}}$ by defining
{\footnotesize{}$k_{f}^{A\Rightarrow1+B}=f\circ\text{id}_{\diamond_{\text{\textbf{Opt}}}}$;}
then we have $\text{fmapOpt}\left(k_{f}\right)=\text{fmap}\,k_{f}\circ\text{deflate}=\text{fmap}\:f\circ\text{fmap}\,\text{id}_{\diamond_{\text{\textbf{Opt}}}}\circ\text{deflate}=\text{fmap}\,f$
\item rewrite eq.\ ({*}) as {\footnotesize{}$\text{fmapOpt}\left(k_{f}\diamond_{\text{\textbf{Opt}}}\text{bop}\,p\right)=\text{fmapOpt}\left(\text{bop}\left(f\circ p\right)\diamond_{\text{\textbf{Opt}}}k_{f}\right)$ }{\footnotesize \par}
\item it remains to show that {\footnotesize{}$k_{f}\diamond_{\text{\textbf{Opt}}}\text{bop}\,p=\text{bop}\left(f\circ p\right)\diamond_{\text{\textbf{Opt}}}k_{f}$ }{\footnotesize \par}
\item use the properties {\footnotesize{}$k_{f}\diamond_{\text{\textbf{Opt}}}q=f\circ q$
and $q\diamond_{\text{\textbf{Opt}}}k_{f}=q\circ\text{fmap}^{\text{Opt}}f$,
and $f\circ\text{bop}\,p=\text{bop}\left(f\circ p\right)\circ\text{fmap}^{\text{Opt}}\,f$
(property from slide 11)}{\footnotesize \par}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Summary: The methods and the laws}

Filterable functors can be defined via \texttt{\textcolor{blue}{\footnotesize{}filter}},
\texttt{\textcolor{blue}{\footnotesize{}deflate}}, or \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}} 
\begin{itemize}
\item All three methods are \emph{equivalent} but have different roles:
\begin{itemize}
\item The easiest to use in program code is \texttt{\textcolor{blue}{\footnotesize{}filter}}
/ \texttt{\textcolor{blue}{\footnotesize{}withFilter}} 
\item The easiest type signature to implement and reason about is \texttt{\textcolor{blue}{\footnotesize{}deflate}} 
\item Conceptually, the laws are easiest to remember with \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}} 
\end{itemize}
\item {*} The 2 laws for \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}}
are the 2 functor laws with a Kleisli ``twist''
\item {*} Category theory accommodates this via a generalized definition
of functors as liftings between ``twisted'' types. Compare:
\begin{itemize}
\item $\text{fmap}:\left(A\Rightarrow B\right)\Rightarrow F^{A}\Rightarrow F^{B}$
\textendash{} ordinary container (``endofunctor'')
\item $\text{contrafmap}:\left(B\Rightarrow A\right)\Rightarrow F^{A}\Rightarrow F^{B}$
\textendash{} lifting from reversed functions
\item $\text{fmapOpt}:\left(A\Rightarrow1+B\right)\Rightarrow F^{A}\Rightarrow F^{B}$
\textendash{} lifting from Kleisli$_{\text{Opt}}$-functions 
\end{itemize}
\item CT gives us some \emph{intuitions} about how to derive better laws:
\begin{itemize}
\item look for type signatures that resemble a generalized sort of ``lifting''
\item look for natural transformations and use the naturality law
\end{itemize}
\item However, CT does not directly provide any derivations for the laws
\begin{itemize}
\item you will not find the laws for \texttt{\textcolor{blue}{\footnotesize{}filter}}
or \texttt{\textcolor{blue}{\footnotesize{}deflate}} in any CT book
\item CT is abstract, only gives hints about possible further directions
\begin{itemize}
\item investigate functors having ``liftings'' with different type signatures
\item replace \texttt{\textcolor{blue}{\footnotesize{}Option}} in the Kleisli$_{\text{Opt}}$
construction by another functor
\end{itemize}
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Structure of filterable functors}


\framesubtitle{How to recognize a filterable functor by its type?}

Intuition from \texttt{\textcolor{blue}{\footnotesize{}deflate}}:
reshuffle data in $F^{A}$ after replacing some $A$'s by $1$
\begin{itemize}
\item ``reshuffling'' usually means reusing different parts of a disjunction
\end{itemize}
Some constructions of exponential-polynomial filterable functors 
\begin{enumerate}
\item $F^{A}=Z$ (constant functor) for a fixed type $Z$ (define $\text{fmapOpt}\,f=\text{id}$)
\begin{itemize}
\item Note: $F^{A}=A$ (identity functor) is \emph{not} filterable
\end{itemize}
\item $F^{A}\equiv G^{A}\times H^{A}$ for any filterable functors $G^{A}$
and $H^{A}$
\item $F^{A}\equiv G^{A}+H^{A}$ for any filterable functors $G^{A}$ and
$H^{A}$
\item $F^{A}\equiv G^{H^{A}}$ for \emph{any} functor $G^{A}$ and filterable
functor $H^{A}$
\item $F^{A}\equiv1+A\times G^{A}$ for a filterable functor $G^{A}$
\begin{itemize}
\item Note: \emph{pointed} types $P$ are isomorphic to $1+Z$ for some
type $Z$
\begin{itemize}
\item Example of non-trivial pointed type: $A\Rightarrow A$
\item Example of non-pointed type: $A\Rightarrow B$ when $A$ is different
from $B$
\end{itemize}
\item So $F^{A}\equiv P+A\times G^{A}$ where $P$ is a pointed type and
$G^{A}$ is filterable
\item Also have $F^{A}\equiv P+A\times A\times...\times A\times G^{A}$
similarly
\end{itemize}
\item $F^{A}\equiv G^{A}+A\times F^{A}$ (recursive) for a filterable functor
$G^{A}$
\item $F^{A}\equiv G^{A}\Rightarrow H^{A}$ if\emph{ }contrafunctor $G^{A}$
and functor $H^{A}$ \emph{both} \emph{filterable}
\begin{itemize}
\item Note: the functor $F^{A}\equiv G^{A}\Rightarrow A$ is not filterable
\end{itemize}
\end{enumerate}
\end{frame}

\begin{frame}{{*} Worked examples II: Constructions of filterable functors I}

(2) The \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}} laws hold
for $F^{A}\times G^{A}$ if they hold for $F^{A}$ and $G^{A}$
\begin{itemize}
\item For $f^{A\Rightarrow1+B}$, get {\footnotesize{}$\text{fmapOpt}_{F}(f):F^{A}\Rightarrow F^{B}$
}and {\footnotesize{}$\text{fmapOpt}_{G}(f):G^{A}\Rightarrow G^{B}$}{\footnotesize \par}
\item Define {\footnotesize{}$\text{fmapOpt}_{F\times G}f\equiv p^{F^{A}}\times q^{G^{A}}\Rightarrow\text{fmapOpt}_{F}(f)(p)\times\text{fmapOpt}_{G}(f)(q)$}{\footnotesize \par}
\item Identity law: $f=\text{id}_{\diamond_{\text{Opt}}}$, so {\footnotesize{}$\text{fmapOpt}_{F}f=\text{id}$}
and {\footnotesize{}$\text{fmapOpt}_{G}f=\text{id}$}{\footnotesize \par}
\begin{itemize}
\item Hence we get $\text{fmapOpt}_{F+G}(f)(p\times q)=\text{id}(p)\times\text{id}(q)=p\times q$
\end{itemize}
\item Composition law:{\footnotesize{}
\begin{align*}
 & (\text{fmapOpt}_{F\times G}\,f_{1}\circ\text{fmapOpt}_{F+G}\,f_{2})(p\times q)\\
=\  & \text{fmapOpt}_{F\times G}(f_{2})\left(\text{fmapOpt}_{F}(f_{1})(p)\times\text{fmapOpt}_{G}(f_{1})(q)\right)\\
=\  & (\text{fmapOpt}_{F}\,f_{1}\circ\text{fmapOpt}_{F}\,f_{2})(p)\times\left(\text{fmapOpt}_{G}\,f_{1}\circ\text{fmapOpt}_{G}\,f_{2}\right)(q)\\
=\  & \text{fmapOpt}_{F}(f_{1}\diamond_{\text{Opt}}f_{2})(p)\times\text{fmapOpt}_{G}(f_{1}\diamond_{\text{Opt}}f_{2})(q)\\
=\  & \text{fmapOpt}_{F\times G}(f_{1}\diamond_{\text{Opt}}f_{2})(p\times q)
\end{align*}
}{\footnotesize \par}
\item Exactly the same proof as that for functor property for $F^{A}\times G^{A}$
\begin{itemize}
\item this is because \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}}
corresponds to a generalized functor
\end{itemize}
\item New proofs are necessary only when using non-filterable functors
\begin{itemize}
\item these are used in constructions 4 \textendash{} 6
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{{*} Worked examples II: Constructions of filterable functors II}

(5) The \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}} laws hold
for $F^{A}\equiv1+A\times G^{A}$ if they hold for $G^{A}$
\begin{itemize}
\item For $f^{A\Rightarrow1+B}$, get {\footnotesize{}$\text{fmapOpt}_{G}(f):G^{A}\Rightarrow G^{B}$}{\footnotesize \par}
\item {\footnotesize{}Define $\text{fmapOpt}_{F}(f)(1+a^{A}\times q^{G^{A}})$
by returning $0+b\times\text{fmapOpt}_{G}(f)(q)$ if the argument
is $0+a\times q$ and if $f(a)=0+b$, and returning $1+0$ otherwise}{\footnotesize \par}
\item Identity law: {\footnotesize{}$f=\text{id}_{\diamond_{\text{Opt}}}$,
so $f(a)=0+a$ and $\text{fmapOpt}_{G}f=\text{id}$}{\footnotesize \par}
\begin{itemize}
\item Hence we get{\footnotesize{} $\text{fmapOpt}_{F}(\text{id}_{\diamond_{\text{Opt}}})(1+a\times q)=1+a\times q$}{\footnotesize \par}
\end{itemize}
\item Composition law: {\footnotesize{}need only to check for arguments
$0+a\times q$, and only when $f_{1}(a)=0+b$ and $f_{2}(b)=0+c$,
in which case $(f_{1}\diamond_{\text{Opt}}f_{2})(a)=0+c$; then 
\begin{align*}
 & (\text{fmapOpt}_{F}\,f_{1}\circ\text{fmapOpt}_{F}\,f_{2})(0+a\times q)\\
=\  & \text{fmapOpt}_{F}(f_{2})\left(\text{fmapOpt}_{F}(f_{1})(0+a\times q)\right)\\
=\  & \text{fmapOpt}_{F}(f_{2})\left(0+b\times\text{fmapOpt}_{G}(f_{1})(q)\right)\\
=\  & 0+c\times(\text{fmapOpt}_{G}\,f_{1}\circ\text{fmapOpt}_{G}\,f_{2})(q)\\
=\  & 0+c\times\text{fmapOpt}_{G}(f_{1}\diamond_{\text{Opt}}f_{2})(q)\\
=\  & \text{fmapOpt}_{F}(f_{1}\diamond_{\text{Opt}}f_{2})(0+a\times q)
\end{align*}
}{\footnotesize \par}
\end{itemize}
This is a ``greedy filter'': if $f(a)$ is empty, will delete all
data in $G^{A}$
\end{frame}

\begin{frame}{{*} Worked examples II: Constructions of filterable functors III}

(6) The \texttt{\textcolor{blue}{\footnotesize{}fmapOpt}} laws hold
for $F^{A}\equiv G^{A}+A\times F^{A}$ if they hold for $G^{A}$
\begin{itemize}
\item {\footnotesize{}For $f^{A\Rightarrow1+B}$, we have $\text{fmapOpt}_{G}(f):G^{A}\Rightarrow G^{B}$
and $\text{fmapOpt}_{F}^{\prime}(f):F^{A}\Rightarrow F^{B}$ (for
use in recursive arguments as the inductive assumption)}{\footnotesize \par}
\item {\footnotesize{}Define $\text{fmapOpt}_{F}(f)(q^{G^{A}}+a^{A}\times p^{F^{A}})$
by returning $0+\text{fmapOpt}_{F}^{\prime}(f)(p)$ if $f(a)=1+0$,
and $\text{fmapOpt}_{G}(f)(q)+b\times\text{fmapOpt}_{F}^{\prime}(f)(p)$
otherwise}{\footnotesize \par}
\item Identity law: {\footnotesize{}$\text{id}_{\diamond_{\text{Opt}}}(x)\neq1+0$},
so {\footnotesize{}$\text{fmapOpt}_{F}(\text{id}_{\diamond_{\text{Opt}}})(q+a\times p)=q+a\times p$ }{\footnotesize \par}
\item Composition law: {\footnotesize{}$(\text{fmapOpt}_{F}(f_{1})\circ\text{fmapOpt}_{F}(f_{2}))(q+a\times p)=\text{fmapOpt}_{F}(f_{1}\diamond_{\text{Opt}}f_{2})(q+a\times p)$}{\footnotesize \par}
\item {\footnotesize{}For arguments $q+0$, the laws for $G^{A}$ hold;
so assume arguments $0+a\times p$. When $f_{1}(a)=0+b$ and $f_{2}(b)=0+c$,
the proof of the previous example will go through. So we need to consider
the two cases $f_{1}(a)=1+0$ and $f_{1}(a)=0+b$, $f_{2}(b)=1+0$ }{\footnotesize \par}
\item {\footnotesize{}If $f_{1}(a)=1+0$ then $(f_{1}\diamond_{\text{Opt}}f_{2})(a)=1+0$;
to show $\text{fmapOpt}_{F}^{\prime}(f_{2})(\text{fmapOpt}_{F}^{\prime}(f_{1})(p))$
$=\text{fmapOpt}_{F}^{\prime}(f_{1}\diamond_{\text{Opt}}f_{2})(p)$,
use the inductive assumption about $\text{fmapOpt}_{F}^{\prime}$
on $p$}{\footnotesize \par}
\item {\footnotesize{}If $f_{1}(a)=0+b$ and $f_{2}(b)=1+0$ then $(f_{1}\diamond_{\text{Opt}}f_{2})(a)=1+0$;
to show $\text{fmapOpt}_{F}(f_{2})(0+b\times\text{fmapOpt}_{F}^{\prime}(f_{1})(p))$
$=\text{fmapOpt}_{F}^{\prime}(f_{1}\diamond_{\text{Opt}}f_{2})(p)$,
rewrite $\text{fmapOpt}_{F}(f_{2})(0+b\times\text{fmapOpt}_{F}^{\prime}(f_{1})(p))$
$=\text{fmapOpt}_{F}^{\prime}(f_{2})(\text{fmapOpt}_{F}^{\prime}(f_{1})(p))$
and again use the inductive assumption about $\text{fmapOpt}_{F}^{\prime}$
on $p$}{\footnotesize \par}
\end{itemize}
This is a ``list-like filter'': if $f(a)$ is empty, will recurse
into nested $F^{A}$ data
\end{frame}

\begin{frame}{Worked examples II: Constructions of filterable functors IV}

Use known filterable constructions to show that{\footnotesize{} $F^{A}\equiv(\text{Int}\times\text{String})\Rightarrow\left(1+\text{Int}\times A+A\times\left(1+A\right)+\left(\text{Int}\Rightarrow1+A+A\times A\times\text{String}\right)\right)$
}is a filterable functor
\begin{itemize}
\item Instead of implementing \texttt{\textcolor{blue}{\footnotesize{}Filterable}}
and verifying laws by hand, we analyze the structure of this data
type and use known constructions
\item Define some auxiliary functors that are parts of the structure of
$F^{A}$,
\begin{itemize}
\item $R_{1}^{A}=\left(\text{Int}\times\text{String}\right)\Rightarrow A$
and $R_{2}^{A}=\text{Int}\Rightarrow A$ 
\item $G^{A}=1+\text{Int}\times A+A\times\left(1+A\right)$ and $H^{A}=1+A+A\times A\times\text{String}$
\end{itemize}
\item Now we can rewrite {\footnotesize{}$F^{A}=R_{1}\left[G^{A}+R_{2}\left[H^{A}\right]\right]$}{\footnotesize \par}
\begin{itemize}
\item $G^{A}$ is filterable by construction 5 because it is of the form
$G^{A}=1+A\times K^{A}$ with filterable functor $K^{A}=1+\text{Int}+A$
\item $K^{A}$ is of the form $1+A+X$ with constant type $X$, so it is
filterable by constructions 1 and 3 with the \texttt{\textcolor{blue}{\footnotesize{}Option}}
functor $1+A$
\item $H^{A}$ is filterable by construction 5 with $H^{A}=1+A\times\left(1+A\times\text{String}\right)$,
while $1+A\times\text{String}$ is filterable by constructions 5 and
1
\end{itemize}
\item Constructions 3 and 4 show that $R_{1}\left[G^{A}+R_{2}\left[H^{A}\right]\right]$
is filterable
\end{itemize}
Note that there is more than one way of implementing \texttt{\textcolor{blue}{\footnotesize{}Filterable}}
here
\end{frame}

\begin{frame}{{*} Exercises II}
\begin{enumerate}
\item Implement a \texttt{\textcolor{blue}{\footnotesize{}Filterable}} instance
for \texttt{\textcolor{blue}{\footnotesize{}type F{[}T{]} = G{[}H{[}T{]}{]}}}
assuming that the functor \texttt{\textcolor{blue}{\footnotesize{}H{[}T{]}}}
already has a \texttt{\textcolor{blue}{\footnotesize{}Filterable}}
instance (construction 4). Verify the laws rigorously (i.e.\ by calculations,
not tests).
\item For \texttt{\textcolor{blue}{\footnotesize{}type F{[}T{]} = Option{[}Int
$\Rightarrow$ Option{[}(T, T){]}{]}}}, implement a \texttt{\textcolor{blue}{\footnotesize{}Filterable}}
instance. Show that the filterable laws hold by using known filterable
constructions (avoiding explicit proofs or tests).
\item Implement a \texttt{\textcolor{blue}{\footnotesize{}Filterable}} instance
for $F^{A}\equiv G^{A}+\text{Int}\times A\times A\times F^{A}$ (recursive)
for a filterable functor $G^{A}$. Verify the laws rigorously.
\item Show that $F^{A}=1+A\times G^{A}$ is in general \emph{not} filterable
if $G^{A}$ is an arbitrary (non-filterable) functor; it is enough
to give an example.
\item Show that $F^{A}=1+G^{A}+H^{A}$ is filterable if $1+G^{A}$ and $1+H^{A}$
are filterable (even when $G^{A}$ and $H^{A}$ are by themselves
not filterable).
\item Show that the functor $F^{A}=A+\left(\text{Int}\Rightarrow A\right)$
is not filterable.
\item Show that one can define \texttt{\textcolor{blue}{\footnotesize{}deflate}}$:C^{1+A}\Rightarrow C^{A}$
for any contrafunctor $C^{A}$ (not necessarily filterable), similarly
to how one can define \texttt{\textcolor{blue}{\footnotesize{}inflate}}$:F^{A}\Rightarrow F^{1+A}$
for any functor $F^{A}$ (not necessarily filterable). 
\end{enumerate}
\end{frame}

\begin{frame}{{*} Bonus slide I: Definition of filterable contrafunctors}

\framesubtitle{When is a contrafunctor filterable?}

When a contrafunctor {\footnotesize{}$C^{A}$} with {\footnotesize{}$\text{contrafmap}:\left(B\Rightarrow A\right)\Rightarrow C^{A}\Rightarrow C^{B}$}
has also
\begin{itemize}
\item \texttt{\textcolor{blue}{\footnotesize{}filter}}/\texttt{\textcolor{blue}{\footnotesize{}withFilter}}{\footnotesize{}$:\left(A\Rightarrow\text{Boolean}\right)\Rightarrow C^{A}\Rightarrow C^{A}$}
\textendash{} same as for functors
\item \texttt{\textcolor{blue}{\footnotesize{}inflate}}{\footnotesize{}$:C^{A}\Rightarrow C^{1+A}$}
and \texttt{\textcolor{blue}{\footnotesize{}contrafmapOpt}}{\footnotesize{}$:\left(B\Rightarrow1+A\right)\Rightarrow C^{A}\Rightarrow C^{B}$}{\footnotesize \par}
\item All three functions are computationally equivalent...
\begin{itemize}
\item {\footnotesize{}$\text{filter}(p^{A\Rightarrow\text{Boolean}})=\text{inflate}^{C^{A}\Rightarrow C^{1+A}}\circ\text{contrafmap}(\text{bop}\,p)$}{\footnotesize \par}
\item {\footnotesize{}$\text{inflate}^{C^{A}\Rightarrow C^{1+A}}=\text{contrafmap}\left(0+x^{A}\Rightarrow x\right)\circ\text{filter}\left(\_\Rightarrow\text{true}\right)$}{\footnotesize \par}
\item {\footnotesize{}$\text{contrafmapOpt}\:f^{B\Rightarrow1+A}=\text{inflate}\circ\text{contrafmap}\,f$}{\footnotesize \par}
\item {\footnotesize{}$\text{inflate}=\text{contrafmapOpt}\,(\text{id}^{1+A\Rightarrow1+A})$}{\footnotesize \par}
\end{itemize}
\item but have different laws
\begin{itemize}
\item 4 laws (naturality, conjunction, identity, partial function) for \texttt{\textcolor{blue}{\footnotesize{}filter}} 
\item 3 laws (naturality, conjunction, identity) for \texttt{\textcolor{blue}{\footnotesize{}inflate}} 
\item 2 laws (identity, contracomposition) for \texttt{\textcolor{blue}{\footnotesize{}contrafmapOpt}} 
\begin{itemize}
\item as before, \texttt{\textcolor{blue}{\footnotesize{}contrafmapOpt}}
is a ``twisted'' version of \texttt{\textcolor{blue}{\footnotesize{}contrafmap}} 
\end{itemize}
\end{itemize}
\item Examples of filterable contrafunctors
\begin{itemize}
\item $C^{A}\equiv A\Rightarrow1+Z$ where $Z$ is a fixed type
\item $C^{A}\equiv1+A\Rightarrow Z$
\end{itemize}
\item Examples of non-filterable contrafunctors
\begin{itemize}
\item $C^{A}\equiv A\times F^{A}\Rightarrow Z$ \textendash{} cannot implement
\texttt{\textcolor{blue}{\footnotesize{}inflate}} 
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{{*} Bonus slide II: Structure of filterable contrafunctors}

\framesubtitle{How to build up a filterable contrafunctor from parts?}
\begin{itemize}
\item Filterable contrafunctors ``can consume fewer data items''
\item The easiest function to consider first is \texttt{\textcolor{blue}{\footnotesize{}inflate}} 
\end{itemize}
Some constructions of filterable contrafunctors:
\begin{enumerate}
\item $C^{A}=Z$ (constant contrafunctor)

Functor constructions (no need to check laws for these): 
\item $F^{A}\equiv G^{A}\times H^{A}$ for any filterable contrafunctor
$G^{A}$ and $H^{A}$
\item $F^{A}\equiv G^{A}+H^{A}$ for any filterable contrafunctor $G^{A}$
and $H^{A}$
\item $F^{A}\equiv G^{H^{A}}$ for $H^{A}$ a filterable (contra)functor
and $G^{A}$ any (contra)functor \textendash{} various combinations
possible here
\item $F^{A}\equiv G^{A}\Rightarrow H^{A}$ if\emph{ }functor $G^{A}$ and
contrafunctor $H^{A}$ \emph{both} \emph{filterable}

Special constructions:
\item $F^{A}\equiv1+A\times G^{A}\Rightarrow H^{A}$ where $G^{A}$ and
$H^{A}$ are filterable
\item $F^{A}\equiv A\times G^{A}\Rightarrow1+H^{A}$ if $G^{A}$ and $H^{A}$
are filterable
\end{enumerate}
\end{frame}

\begin{frame}{Addendum}

\framesubtitle{Notes added after the tutorial was complete}
\begin{itemize}
\item A polynomial functor $F^{A}$ is filterable if and only if it can
be expressed (isomorphically) as $F^{A}=C\times\left(1+...\right)$
where $C$ is a constant type. An example of a polynomial functor
not of this form is $F^{A}=P+Q\times A$, where $P\neq Q$ are constant
types and $P$ is not pointed (not known to be isomorphic to $1+Z$
for some type $Z$).
\item Given a polynomial functor $F^{A}$, one can decide algorithmically
whether $F^{A}$ is filterable, and derive \emph{some} implementation
of \texttt{\textcolor{blue}{\footnotesize{}deflate}} or \texttt{\textcolor{blue}{\footnotesize{}withFilter}}
such that the laws hold. However, typically there will be many legitimate
implementations, and the application-specific filtering requirements
are not obviously guessable in advance.
\end{itemize}
\end{frame}

\end{document}
